Lambda the Ultimate

Either I cannot search, or the term has web-unfriendly name, but it's pretty tough to look for lambda-mu calculus, even in scope of LtU only.

For example, did we discuss this paper or related?

Control Categories and Duality: on the Categorical Semantics of the Lambda-Mu Calculus Just one of the results:

As a corollary, we obtain a syntactic duality result: there exist syntactic translations between call-by-name and call-by-value which are mutually inverse and which preserve the operational semantics.

...and...

It is interesting to compare this with Filinski’s work, in which he obtains a duality result by working with a larger and more symmetric syntax, in which the dual of a term is essentially its mirror image.

Also, is Parigot's Lambda-mu-calculus: an algorithmic interpretation of classical natural deduction available online anywhere (except ACM)?

---

[on edit: aha, found one reference (actually a pair forming one reference): Call-by-Value is Dual to Call-by-Name and Call-by-value is Dual to Call-by-name, Reloaded ("We consider the relation of the dual calculus of Wadler to the lambda-mu-calculus of Parigot")]

I hope this isn't off topic. It seems a very large number of text files are some sort of delimited files (.csv, .tab, etc.). Awk seems to expect these files and cleanly allows dealing with only specific 'fields' in the file. Have there been any attempts to introduce some sort of (easy to use) meta data which describes layout of the file...perhaps more importantly the type of data in it. Excel or specific database files are obviously tied to the application that created them.

XML works well here...it defines data types and some relationship among data points, but is too verbose (a file with 5 columns but thousands of lines would be many times larger if xmlized).

I've come accross some information about type systems which describe memory layout (...which I don't really understand yet)...could something like that also be used to describe disk files?

Related to the recent "how to read papers" thread...

How do you guys organize your papers? I have a file naming scheme that's a big pain to manage and not terribly useful. I guess what I want is something like iPapers, but less tied to PubMed and cross-platform. (At least I need it to run on my Linux workstation, and hopefully on my Mac laptop...) And I guess in my dirtiest fantasies it would maybe integrate with Citeseer and CiteULike, but that's not so important to me, actually.

I'm sure semantic web types will tell me that I really want a general purpose RDF browser or something to manage general meta-data, but I'd be happy with something less general and more tailored to this domain.

Anyway, does anybody out there have a tool (or just an organizational discipline) that they're happy with? Satisfy my curiosity...

Dyna is a language I stumbled upon by accident today. What I find interesting qualities of it are its claimed clean compilation to C++ and its non-standard semantics.

Dyna is a small, very-high-level programming language that makes it easy to specify dynamic programs and train their weights. You write a short declarative specification in Dyna, and the Dyna optimizing compiler produces efficient C++ classes that form the core of your C++ application.

Natural applications in NLP include various kinds of parsing, machine translation, speech decoding, and finite-state modeling. Dyna also has many other applications, especially in other applied AI areas, since dynamic programming (and its degenerate case, tree search) is a common strategy for solving combinatorial optimization problems.

Properly speaking, Dyna is a "weighted" logic programming language: terms have values, and Horn clauses are replaced by aggregation equations. It is Turing-complete. You can also think of Dyna as extending compiled C++ with powerful deductive database features.

What languages do we wish were still maintained? My list starts:

• Charity
• Cayenne
• O'Haskell
• Kiev
• Cecil

In
this paper, we present a typeful approach to implementing objects that makes use of a recently introduced notion of guarded datatypes. In particular, we demonstrate how the feature of multiple inheritance can be supported with this approach, presenting a simple and general account for multiple inheritance in a typeful manner.

[snip]

We refer the reader to [XCC03,Xi02] for further details on this typeful approach to OOP (with single inheritance). The treatment of multiple inheritance in this paper bears a great deal of similarity to the treatment of single inheritance in [XCC03,Xi02], though there are also some substantial differences involved. In order to handle multiple inheritance, we are to treat a path from a (super) class to a (sub)class as a first-class value.

I was thinking of possibly making all functions in the Heron programming language into classes with a single public field named "result". I was wondering what other languages do similar things to this, and what the advantages / disadvantages might be of such as approach.

I have posted an example of Heron code which would model this apporach at http://www.artima.com/weblogs/viewpost.jsp?thread=116558

Thanks in advance!

I'm trying to write a denotational semantics and I'm having a problem. I seem to only be able to express what I want by writing code that generates code, rather than just writing code. By "code" I mean my lambda-calculus-like definitional language. (Actually I plan to use Haskell for this and thus get a semantics and a reference implementation "for free" but I digress.)

Anyway, I could give specifics, and perhaps the question doesn't make sense without specifics (if so, I'll be glad to post what I have) but I wonder if anyone has some high-level comments on this type of problem.

It seems like a general problem in programming not specific to denotational semantics, actually. It seems like the idea of generative programming accomodates the need to generate code at compile-time, but I'm not as familiar with efforts to accomodate run-time ("dynamic") code generation. LISP macros? For one thing this style of programming requires the language to have an "eval" function or similar, or requires the program to ship with a compiler.

Before I saw C++ templates, I generally considered generating code to be a sign of weakness of the programmer and/or the language, because my primary example was C with the C preprocessor. Now I've changed my mind, and I wonder whether we try to put too much into languages whereas we could somehow have simpler languages with more powerful code generation facilities.

Oh well, I'm kind of rambling at this point, so I'll stop since I've probably provided plenty of fodder for feedback.

Epigram system, being invented by Conor McBride, is an implementation of dependently typed functional programming language Epigram, designed by Conor McBride himself and James McKinna. (See their paper The View From The Left). Good Epigram tutorial you can find here. Also see Wikipedia.

Being not fully content with editing capabilities of currently available version of Epigram system, a.k.a. Durham Epigram, I decided to develop my own editor for Epigram language using a tool called MPS. I named my editor MPgram.

At the moment, I've already written something of MPgram which is able to be played with, and I created a page for MPgram, where MPgram is available for everyone to download.
http://www.jetbrains.net/confluence/display/MPS/Epigram

The best place to feed back is MPS EAP forum, I think.

Here's a question I've promoted from another thread (sorry for the multiple postings).

What's the difference between static type inference (like in Haskell) and a latent (tagged) type system (think Scheme) with a real good partial evaluator? In the type-inference situation, we're using unification to solve a set of constraints. If there's no solution, we give up and say the program was ill-typed. On the other hand, it seems like tag checking code in a latently typed lanugage would be a good candidate to get partially evaluated away at compile time. For example it seems like...

;; typed values are really pairs of values and types
;; e.g. (123 . 'number)
;;      ("abc" . 'string)
(define (isnumber n) (eq? (cdr n) 'number))
(define (add arg1 arg2)
    (if (and (isnumber arg1) (isnumber arg2))
        (machine-add (car arg1) (car arg2))
        (error "not a number")))

(add '(4 . number) '(5 . number))

...should be easily changed into...

(machind-add 4 5)

... And after we're done partially evaluating our source, if we still have left over type-check predicates like 'isnumber' in the code then we again declare that the program is ill-typed. Are the two methods comparable in any way? Is one method more powerful than the other, or are they somehow duals of each other? Are there any papers available discussing this?

Anton van Straaten recommends looking at a previous typing thread, and the paper Types as Abstract Interpretations, as well as a posting of his to the LL mailing list. Any futher thoughts?